fpf{-}val(${\it eq}$; $f$; $x$; $a$,$z$.$P$($a$;$z$)) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\uparrow$fpf{-}dom(${\it eq}$; $x$; $f$)) $\Rightarrow$ $P$($x$;$f$${\it eq}$($x$))